YES(?,O(1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

TcT has computed following constructor-restricted linear polynomial
interpretation.

This order satisfies following ordering constraints


Hurray, we answered YES(?,O(1))